Nuprl Lemma : es-real-implies 11,40
P:(ES{i}{i'}), p:es-real{i:l}(es.P(es)), es:ES{i}. Consistent(es-realizer(p);es)  P(es) 
latex

Definitionst  T, P  Q, x:A. B(x), es-realizer(p), x:A  B(x), P & Q, R ||- es.P(es), x:A. B(x), es.P(es), Type, , ES, x:AB(x), f(a), x(s), x. t(x), x.A(x), Consistent(R;es)
LemmasR-consistent wf, es-realizer wf, es-real wf, event system wf

origin